Flight-critical software is part of an aircraft system that includes sensors and actuators, and integrates physical processes with computation. This software controls and interacts with many different, mixed-criticality subsystems, such as the engine, guidance and navigation, fuel management, flight control, communication, collision detection and resolution, climate control, and entertainment.
The algorithms underlying the software are based on mathematical principles such as algebra, analysis, geometry, and trigonometry. The calculations often involve nonlinear arithmetic that is not adequately supported by formal tools due to the complexity of the necessary calculations. Typically, models based on continuous mathematics are implemented using discrete software systems. In such models, numeric values are approximated by floating-point representations that introduce errors. Floating-point computations can likewise introduce errors. In addition, the software itself is executed on a distributed platform that introduces numerical and timing errors due to jitter, sensor precision, and external mechanical or functional errors.
These errors can accumulate and may qualitatively change the behavior of the system. Any time the system must make a decision (e.g., an if-then-else or loop construct) that compares two values, either or both of those values may be offset by error to some degree. This can cause a system to perform different behaviorally than if the values were precisely represented. The value around which execution changes is called a “behavioral pivot value.” Decisions that depend on behavioral pivot values can affect the timing behavior and physical performance of the system controlled by the software. However, current tools either do not take these errors into account or are not scalable enough to support industrial-sized problems.